As more traffic-voice and e-commerce-migrates to Internet Protocol-based networks, it has become essential to ensure that the systems making up this important infrastructure be reliable. The reliability target for today's Internet processing engines is what's called "five-nines" (up 99.999 percent of the time).
As part of our product development, Cisco Systems' high-end core router group routinely integrates error-correcting circuits (ECCs) into designs. These blocks of code, which are commonly used in networking, perform the critical functions of verifying and correcting data streams. Once developed, the ECCs are often used multiple times in a single design and can become part of numerous high-end routers.
The critical nature of the ECCs makes functional verification crucial. This article describes how our design group uses symbolic simulation, which is a semiformal verification technique, to verify our ECCs. It covers the application of symbolic simulation to the two types of ECC blocks most commonly used by the high-end router group: (255,251) Reed-Solomon (RS) code and distance-3 Hamming code. Both codes are single-error-correcting and double-error-detecting.
We were directed to apply formal techniques to rigorously prove the correctness of our ECC blocks. However, ECCs are complex and difficult to formally verify. For example, the RS encoder/decoder has complex feedback loops, numerous memory elements/flops and arithmetic transformations.
Binary simulation, which is tightly embedded into our group's verification flow, allows only limited coverage, leaving many "holes" in the verification process. Formal proof would have required exhaustive simulation, involving trillions of vectors-which would have taken years to complete.
Model checking was considered as an alternative. However, model checkers are limited by the number of state elements in the design, require a proprietary language and can be difficult to integrate into an existing design flow. We believe that model checkers are useful for state machines and random logic but not suited to data-oriented designs like ECCs, which encode and decode data streams. Although the number of flip-flops is large, the state space they represent is sparse.
Equivalence checking is another popular formal way to verify an implementation against its specification. This technique was not considered because we were concerned with the formal verification of the specification itself. Our inputs were register-transfer-level (RTL) implementations of the encoding and decoding algorithms of the ECC codes.
We learned about a novel semiformal verification method called symbolic simulation. The methodology was first described by IBM in 1979 and, in 1985, a professor at Carnegie Mellon University created the first working, bit-level symbolic simulator. The technology is being used in internally developed symbolic simulators at Intel and other companies.
Symbolic simulation does not explore the state space, is not limited by the number of flops and is considered very effective for data-oriented designs. It is the enabling technology for InnoLogic Systems' ESP tool, which Cisco Systems purchased and used for the verification described in this article.
Symbolic simulation allows designers to simulate multiple binary vectors (or vector streams) together as one simulation. This is achieved by allowing the simulator to accept "symbols" as inputs just like binary 0 or 1. These symbols represent both values 0 and 1 simultaneously on the input to which they are applied. Like binary simulation, symbolic simulation requires a testbench to apply input stimulus and check output results. The only difference is that symbols need to be applied as inputs wherever desired in a symbolic simulation testbench. The advantage of symbolic simulation is that 2n (n=number of symbols) equivalent binary vectors are investigated simultaneously.
Reed-Solomon codec
Verification of the RS encoder is straightforward. Symbolic simulation allows easy verification by applying symbols at the data inputs and checking for a legal code word at the output. The verification of the RS decoder, however, is more interesting.
We divided the input space of the decoder into 1) legal code words, 2) legal code words with exactly one error, 3) legal code words with exactly two errors and 4) the rest of the input space. We then created a symbolic testbench for the first three scenarios. Some work was required to constrain a set of input symbols to the required input space in each case.
Since the output code is single-error-correcting, the first two testbenches check that the legal code word output is always 1 and the third testbench checks that this output is always 0 (i.e., no double error is erroneously detected as a legal code word). Additionally, for the first two testbenches, expected legal code words are precalculated in terms of the input symbols. The decoded output is checked against those expected legal code word expressions. Fig. 1 illustrates our verification flow.
The testbench example shown in Fig. 2 applies to the second category described above (legal code words with exactly one error). It illustrates how to check the correctness of the Reed-Solomon decoder for 1-byte errors. It instantiates the error injector, the Reed-Solomon decoder and the expected output calculator. The 8-bit symbol [I]inject_e_loc_sym[I] controls the byte where the error will be injected. By making it symbolic, all possible 1-byte error locations are covered.
Similarly, the 8-bit symbol [I]inject_e_vec_sym[I] covers all possible errors that can happen at a byte location. In addition, 251 data bytes are injected as symbols to the error injector. The output of the error injector is a sequence of 255 bytes (251 data bytes + 4 Reed-Solomon parity bytes), which covers all possible 1-byte errors. This output is applied as input to the decoder. Finally, the decoded output and error flags are checked for consistency against expected output.
The fourth category (the rest of the input space) is not of interest to us as the decoder is allowed to behave arbitrarily in that scenario. However, we created a testbench with symbolic inputs representing all code words with exactly three errors. The simulation of this testbench showed to us that more than 99.99 percent of this input space is still detected as illegal by the decoder.
Figure 2
We were also able to obtain a binary vector (representing a code word with three errors) that was erroneously decoded as if it were a legal code word. We could never have found this vector with a binary simulator. This exercise let us characterize the performance of our RS decoder and gave us confidence in its robustness under inputs which break its correctness.
Hamming codec
Single-error-correction double-error-detection (Secded) Hamming code is widely deployed across various hardware groups to protect most of the data stored in memories. We implemented a C program to generate a Hamming codec implementation parameterized by the data size. Since each chip's timing and area constraints are different, this program provides various options to synthesize different implementations of Hamming code. In addition, it allows for manual modification of the generated RTL to make sure that a designer's specific constraints are met.
The complexity of the generating program and possibility of manual modification create a verification problem for these codecs.
We found that InnoLogic's ESP tool was able to verify these generated ECCs in a matter of seconds with a simple testbench. This testbench checked for correctness of Sec and Ded properties of the generated codec. For example, with a 32-bit data size, the Sec and Ded properties take 10 seconds and 30 megabytes each to be completely verified. Our familiarity with Verilog and the tool's familiar event-driven Verilog semantics helped us to easily write the required testbench.
We took our verification a step further by automatically generating a symbolic simulation testbench along with the codec from the generator program. With this approach, the user can generate a codec of his or her specification and use the generated testbench to formally verify it, spending negligible time on the verification process. Any manual changes to the codec can also be verified by the same testbench. The increased productivity that this capability gave us led to the popular adoption of the generator across various groups.
The merits of symbols
By combining event-driven simulation with Boolean expression propagation, symbolic simulation offers a formal simulation approach that provides more complete coverage with a fraction of the cycles required by traditional simulation.
As symbolic simulation is very similar to traditional simulation, it was simple to learn. In fact, we had our first working testbench (in our design environment) running in a matter of hours without any vendor help. One key advantage was that there were no new languages to learn. We were able to write the properties and the design intent with Verilog, using semantics familiar to us.
For the Reed-Solomon codec, we were allocated about a month for formal verification. We were able to complete it in 25 percent of the allocated time. The productivity gain was tremendous and helped us complete the task well ahead of schedule. Productivity was also gained by embedding symbolic simulation in the Hamming codec generation program.
The greatest limitation we found in using symbolic simulation is that it requires a user-generated testbench to drive the design under test. The testbench must be well-thought-out and written correctly for the results to have any meaning. This process is prone to manual errors.
This approach was unfamiliar to us and, therefore, not easy at first; but we gradually gained expertise in rationalizing testbenches. Help from the vendor was required in the case of Reed-Solomon codec verification because of capacity limitations of the ESP tool. In the testbench we initially created, the encoder and decoder were hooked back to back. However, the complexity of cascaded logic made the symbolic expressions very large and the tool ran out of capacity.
We wrote a separate error injector and were able to reduce the number of symbols by deciding which symbols were really needed (and which were not) for the verification task.
Symbolic simulation is now a regular part of our ECC verification flow. Any changes to the Reed-Solomon codec are regressed using the ESP tool. Also, the Hamming codec generator automatically generates a symbolic simulation testbench, allowing designers who instantiate these blocks to test the block in seconds as a part of their verification flow. This flow has made it much easier for us to modify and improve the generator and we have confidence that the change does not generate faulty ECCs. As a result, we have seen the number of designers using this generator and verification scheme gradually growing in our hardware groups.
In our opinion, designs involving data movement, data pipelines and memory-based designs are well-suited to symbolic simulation. For control and random logic, we believe that model checking may be the better technology.
We recommend that hardware designers and verification engineers consider symbolic simulation as another weapon in their arsenal to attack the bugs that lurk in their designs.
---
Sriram C. Krishnan and Hetal Jariwala are engineers at Cisco Systems Inc. Krishnan holds a PhD in EE and CS from the University of California, Berkeley, and Jariwala an MSEE from the University of Southern California. Gagan Hasteer, product manager at InnoLogic Systems Inc., has a PhD in CS from the University of Illinois.
http://www.isdmag.com
Copyright © 2002 CMP Media LLC
4/1/02, Issue # 14154, page 36.
